﻿/*============================================
 * 类名 :LawFactory
 * 描述 :用于产生运算的工厂类
 *   
 * 创建时间: 2010-1-25 19:30:37
 *============================================*/
using System;
using System.Collections.Generic;

using System.Text;

namespace 命题证明
{
    /// <summary>用于产生运算的工厂类</summary>
    class LawFactory
    {
        /// <summary>用于产生最初步的推理定理</summary>
        public static List<Law> CreateProof()
        {
            //┐  ∧   ∨   →    ↔
            List<Law> laws = new List<Law>();

            #region "会引起条件膨胀的定律"

            // laws.Add( new Law( "a∧b", "b∧a", "交换律" ) );
            // laws.Add( new Law( "a∨(b∧c)", "(a∨b)∧(a∨c)", "分配律" ) );
            // laws.Add( new Law( "a∧(b∨c)", "(a∧b)∨(a∧c)", "分配律" ) );

            //// laws.Add( new Law( "a", "a∨b", "附加律" ) );
            // laws.Add( new Law( "(a∧b)∧c", "a∧(b∧c)", "结合律" ) );

            #endregion


            #region "推理定律"

            laws.Add( new Law( "a∧b", "a", "化简律" ) );
            laws.Add( new Law( "(a↔b)∧a", "b", "等价" ) );
            laws.Add( new Law( "(a→b)∧a", "b", "假言推理" ) );
            laws.Add( new Law( "(a→b)∧(a→┐b)", "┐a", "归谬论" ) );
            laws.Add( new Law( "(a→b)∧┐b", "┐a", "拒取式" ) );
            laws.Add( new Law( "(a∨b)∧┐b", "a", "析取三段论" ) );
            laws.Add( new Law( "(a→b)∧(b→c)", "(a→c)", "假言三段论" ) );
            laws.Add( new Law( "(a↔b)∧(b↔c)", "(a↔c)", "等价三段论" ) );
            laws.Add( new Law( "(a→b)∧(c→d)∧(a∨c)", "b∨d", "构造性二难" ) );
            laws.Add( new Law( "(a→b)∧(c→d)∧(┐b∨┐d)", "┐a∨┐c", "破坏性二难" ) );

            #endregion

            return laws;
        }

        /// <summary>用于产生最基本的等值定律</summary>
        public static List<Law> CreateEqual()
        {
            #region "等值演算"
            List<Law> laws = new List<Law>();
            laws.Add( new Law( new LawFormat( "a┐┐", "a" ), "双重否定律" ) );
            laws.Add( new Law( "a∨a", "a", "幂等律" ) );
            laws.Add( new Law( "a∧a", "a", "幂等律" ) );
          //  laws.Add( new Law( "a∨b", "b∨a", "交换律" ) );
            //laws.Add( new Law( "a∨b∨c", "a∨c∨b", "交换律" ) );
            //laws.Add( new Law( "a∨b∨c", "b∨a∨c", "交换律" ) );
            //laws.Add( new Law( "a∨b∨c", "b∨c∨a", "交换律" ) );
            //laws.Add( new Law( "a∨b∨c", "a∨a∨b", "交换律" ) );
            //laws.Add( new Law( "(a∨b)∨c", "a∨(b∨c)", "结合律" ) );

            laws.Add( new Law( "┐(a∨b)", "┐a∧┐b", "德摩根律" ) );
            laws.Add( new Law( "┐(a∧b)", "┐a∨┐b", "德摩根律" ) );
            laws.Add( new Law( "a∨(a∧b)", "a", "吸收律" ) );
            laws.Add( new Law( "a∧(a∨b)", "a", "吸收律" ) );
            laws.Add( new Law( "a∨1", "1", "零律" ) );
            laws.Add( new Law( "a∧0", "0", "零律" ) );
            laws.Add( new Law( "a∨0", "a", "同一律" ) );
            laws.Add( new Law( "a∧1", "a", "同一律" ) );
            laws.Add( new Law( "a∨(┐a)", "1", "排中律" ) );
            laws.Add( new Law( "a∧(┐a)", "0", "矛盾律" ) );
            laws.Add( new Law( "a→b", "┐a∨b", "蕴涵等值式" ) );
          //  laws.Add( new Law( "┐a∨b", "a→b", "蕴涵等值式" ) );
            laws.Add( new Law( "(a→b)∧(b→a)", "a↔b", "等价等值式" ) );
            laws.Add( new Law( "a↔b", "(a→b)∧(b→a)", "等价等值式" ) );
            laws.Add( new Law( "┐a↔┐b", "a↔b", "等价否定等值式" ) );

            #endregion

            #region "会引起条件膨胀的定律"
            // 
            #endregion

            return laws;
        }

    }
}
